Nuprl Lemma : fpf-dom-type2
11,40
postcript
pdf
X
,
Y
:Type,
eq
:EqDecider(
Y
),
f
:
x
:
X
fp
Top,
x
:
Y
.
strong-subtype(
X
;
Y
)
{(
x
dom(
f
))
(
x
X
)}
latex
Definitions
{
T
}
Lemmas
fpf-dom-type
origin
X, Y:Type, eq:EqDecider(Y), f:x:X fp
Top, x:Y.
{(
x 
dom(f)) (x X)} X, Y:Type, eq:EqDecider(Y), f:x:X fp Top, x:Y.
{(x dom(f)) (x X)}